#!/usr/bin/env python
# encoding: utf-8


"""
@file: sanjiaoxing_zhengming.py
@time: 2017/5/14 下午11:14
"""
# 三角形证明的问题

from mathsolver.functions.base import *
from sympy import expand_trig, symbols, cos, sin, tan, cot
from mathsolver.functions.sanjiao import sanjiaoxing_utils as sjx_u
from mathsolver.functions.sanjiao.sanjiaoxingqiuzhi import (condition_deep_deduce_v2, extract_kd_steps_and_labels,
                                                            extract_af_steps_and_labels)
from mathsolver.functions.sanjiao.triangle_prove_actions import one_cond_actions


# 三角形证明001 知道一个条件，证明另外一个条件
# Input paramer1:等式BaseEq() 要证明的条件
class SanJiaoXingZhengMing001(BaseFunction):
    def solver(self, *args):
        self.label.add('三角形证明')
        prove_eqs = args[0].sympify()
        self.steps.append(['证明:', ''])
        _A, _B, _C = symbols('A, B, C')
        _a, _b, _c, _r = symbols('a, b, c, r')
        tan_subs = ((tan(_A), sin(_A) / cos(_A)), (tan(_B), sin(_B) / cos(_B)), (tan(_C), sin(_C) / cos(_C)))
        cot_subs = ((cos(_A), cos(_A) / sin(_A)), (cot(_B), cos(_B) / sin(_B)), (cot(_C), cos(_C) / sin(_C)))
        sin_subs = ((sin(_A), _a / 2 * _r), (sin(_B), _b / 2 * _r), (sin(_C), _c / 2 * _r))
        cos_subs = ((cos(_A), (_b ** 2 + _c ** 2 - _a ** 2) / (2 * _b * _c)),
                    (cos(_B), (_a ** 2 + _c ** 2 - _b ** 2) / (2 * _a * _c)),
                    (cos(_C), (_a ** 2 + _b ** 2 - _c ** 2) / (2 * _a * _b)))
        left, right = prove_eqs
        prove_f = left - right
        known_eqs = sjx_u.known_triangle_eqs(self.known)
        triangle_eqs = []
        for k, v in known_eqs.sympify():
            k = k.subs(sjx_u.get_triangle_subs())
            v = v.subs(sjx_u.get_triangle_subs())
            triangle_eqs.append([k, v])
        if len(triangle_eqs) != 1:
            raise Exception('Type Match Error')
        cond_eq = triangle_eqs[0]
        # triangle_eq_converts, kds = condition_deep_deduce(BaseEq(cond_eq))  # 条件的转换
        triangle_eq_converts, kds = condition_deep_deduce_v2(BaseEq(cond_eq))  # 条件的转换
        finished = False
        labels = []
        steps = []
        # 先用自动推理 看能不能退出来
        for cond_eq, kd in zip(triangle_eq_converts, kds):
            tmp_f = sympify(cond_eq[0]) - sympify(cond_eq[1])
            if simplify(prove_f / tmp_f) in (1, -1):  # 如果条件转换就已经可以求出，那么就不需要再action函数了
                kd_steps, kd_labels = extract_kd_steps_and_labels(kd)
                steps.extend(kd_steps)
                labels.extend(kd_labels)
                steps.append(['\\therefore ', BaseEq([left, right]).printing()])
                finished = True
                break
        # 如果推不出来 在启用射边角
        for cond_eq, kd in zip(triangle_eq_converts, kds):
            if finished:
                break
            for action_func in one_cond_actions:
                try:
                    action_result, af = action_func(BaseEqs([cond_eq, ]))
                    if not action_result:
                        continue
                    subs = action_result.items()
                    left_subs = left.subs(subs)
                    right_subs = right.subs(subs)
                    if left_subs == right_subs:
                        af_steps, af_labels = extract_af_steps_and_labels(af)
                        steps.extend(af_steps)
                        labels.extend(af_labels)
                        steps.append(['\because ', BaseEqs(subs).printing()])
                        steps.append(
                            ['\therefore ',
                             BaseEq([left, left_subs]).printing() + '且' + BaseEq([right, right_subs]).printing()])
                        steps.append(['\therefore ', BaseEq([left, right]).printing()])
                        finished = True
                        break
                    else:
                        left_subs = expand_trig(left).subs(tan_subs).subs(cot_subs).subs(sin_subs).subs(cos_subs)
                        right_subs = expand_trig(right).subs(tan_subs).subs(cot_subs).subs(sin_subs).subs(cos_subs)
                        left_subs2 = left_subs.subs(subs)
                        right_subs2 = right_subs.subs(subs)
                        if left_subs2 == right_subs2:
                            af_steps, af_labels = extract_af_steps_and_labels(af)
                            steps.extend(af_steps)
                            labels.extend(af_labels)
                            if left_subs != left:
                                steps.append([BaseEq([left, left_subs]).printing(), ''])
                            if right_subs != right:
                                steps.append([BaseEq([right, right_subs]).printing(), ''])
                            steps.append(['因为:', BaseEqs(subs).printing()])
                            steps.append(['所以', BaseEq([left_subs, left_subs2]).printing()])
                            steps.append(['   ', BaseEq([right_subs, right_subs2]).printing()])
                            steps.append([BaseEq([left, right]).printing(), ''])
                            finished = True
                            break
                except Exception:
                    pass
        for label in labels:
            self.label.add(label)
        self.steps.extend(steps)
        return self


class SanJiaoXingZhengMing(BaseFunction):
    CLS = [SanJiaoXingZhengMing001, ]

    def solver(self, *args):
        _solver = None
        for cl in SanJiaoXingZhengMing.CLS:
            try:
                _solver = cl(known=self.known).solver(*args)
            except Exception:
                pass
        if not _solver:
            raise Exception('Can not prove the question')
        return _solver


if __name__ == '__main__':
    pass
